Skip to content

measurable bigmax - #2092

Merged
affeldt-aist merged 1 commit into
math-comp:masterfrom
affeldt-aist:measurable_20260823
Aug 27, 2026
Merged

measurable bigmax#2092
affeldt-aist merged 1 commit into
math-comp:masterfrom
affeldt-aist:measurable_20260823

Conversation

@affeldt-aist

Copy link
Copy Markdown
Member
Motivation for this change

Easy lemma about measurability and bigmax used to reason about the matrix norm.

Checklist
  • added corresponding entries in CHANGELOG_UNRELEASED.md

- [ ] added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

  • PRs with several commits that make sense individually and that
    all compile are preferentially merged into master.
  • PRs with disorganized commits are very likely to be squash-rebased.
Reminder to reviewers

@affeldt-aist affeldt-aist added this to the 1.18.0 milestone Aug 23, 2026
@affeldt-aist affeldt-aist added the enhancement ✨ This issue/PR is about adding new features enhancing the library label Aug 23, 2026

@holgerthies holgerthies left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good to me.

@affeldt-aist

Copy link
Copy Markdown
Member Author

@holgerthies Thanks for having take a look!

@affeldt-aist
affeldt-aist merged commit 45cff6a into math-comp:master Aug 27, 2026
69 checks passed
@affeldt-aist
affeldt-aist deleted the measurable_20260823 branch August 27, 2026 02:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

enhancement ✨ This issue/PR is about adding new features enhancing the library

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants